$\forall$$k$:Knd, $l$:IdLnk, ${\it dt}$:fpf(Id; $x$.Type).
\\[0ex]($\uparrow$fpf{-}dom(Kind{-}deq; $k$; lnk{-}decl($l$; ${\it dt}$)))
\\[0ex]$\Rightarrow$ sqequal(fpf{-}ap(lnk{-}decl($l$; ${\it dt}$); Kind{-}deq; $k$); fpf{-}ap(${\it dt}$; id{-}deq; tag($k$)))